EventsWithValues
== E:Type
== EqDecider(E)
== pred?:(E(E+Unit))
== info:(E(IdId+(IdLnkE)Id))
== EOrderAxioms(E; pred?; info)
== T:(IdIdType)
== when:(x:Ide:ET(loc(e),x))
== after:(x:Ide:ET(loc(e),x))
== (e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e))))
== V:(KndIdType)
== (e:EV(kind(e),loc(e)))
== Top 

latex

---

clarification:

EventsWithValues{i}
== E:Type{i}
== EqDecider(E)
== pred?:(E(E+Unit))
== info:(E(IdId+(IdLnkE)Id))
== EOrderAxioms{i}(E;
== EOpred?;
== EOinfo)
== T:(IdIdType{i})
== when:(x:Ide:ET(loc(info;e),x))
== after:(x:Ide:ET(loc(info;e),x))
== (e:E. first(pred?;e)  (x:Id. when(x,e) = after(x,pred(pred?;e))  T(loc(info;e),x)))
== V:(KndIdType{i})
== (e:EV(kind(info;e),loc(info;e)))
== Top 

latex

Definitions	EqDecider(T), Unit, left+right, IdLnk, EOrderAxioms(E; pred?; info), P  Q, A, b, first(e), x:A. B(x), s = t, pred(e), Knd, Id, Type, x:AB(x), x:AB(x), f(a), kind(e), loc(e), Top
FDL editor aliases	EVal